Abstract: Due to the limitation of system resources, the embedded operating system in the spacecraft does not have the file system module. The system task completes the reading and writing of external storage devices by directly calling the I/O interface. However, with the complexity of space missions, the equipment without a file system will have a large performance bottleneck. Therefore, the development of a safe and reliable file system is an urgent issue for space embedded systems. The space embedded operating system is a typical safety critical system, and every module integrated in the system needs to undergo rigorous testing to ensure that it will not cause malfunctions during operation. The use of formal verification technology can strictly guarantee the correctness of a certain system module mathematically. Therefore, the formal technology is used to verify the correctness of its internal logic according to the requirements of space vehicle file system in this paper.

Key words: software requirements, formal verification, file system, embedded system